/*
 * FastCC.h
 *
 *  Created on: May 9, 2011
 *      Author: trungtq
 */

#ifndef FASTCC_H_
#define FASTCC_H_

#include <vector>
#include <map>
#include <utility>
#include "Equation.h"
#include "Term.h"
#include "Utils.h"
#include "Forest.h"

typedef vector<EquationList>                        PendingList;
typedef map<Term, Term, TermCompare>                RepresentativeMap;
typedef map<Term, TermList, TermCompare>            ClassList;
typedef map<Term, EquationList, TermCompare>        UseLists;
typedef map<TermPair, Equation, TermPairCompare>    LookupTable;

// used for algorithm in paper 2003 - CongruenceClosure with Integer Offsets
typedef map<TermPair, Term, TermPairCompare>        OtherLookupTable;   // delete later

class FastCC {
public:
    FastCC();
    virtual ~FastCC();

private:
    //
    FunctionSet funcSet;
    VariableSet varSet;
    TermSet flattenerSet;
    TermMap flattenMap;

    Forest forest;
    NodeSet nodes;

    //
    PendingList pendingList;
    RepresentativeMap representMap;
    ClassList classLists;
    UseLists useLists;
    LookupTable lookupTable;
    OtherLookupTable otherLookupTable;  // delete later

private:
    /* getter & setter */
    // pending list
    bool isPendingListEmpty();
    EquationList removeLastElementFromPendingList();
    void addElementToPendingList(EquationList pendingElement);

    // representative
    Term getRepresentative(Term term);
    void setRepresentative(Term term, Term represenative);

    // ClassList
    TermList getClassList(Term representative);
    int sizeOfClassList(Term representative);
    void addTermToClassList(Term representative, Term term);
    Term removeLastTermFromClassList(Term representative);

    // UseList
    EquationList getUseList(Term representative);
    int sizeOfUseList(Term representative);
    void addEquationToUseLists(Term representative, Equation equation);
    Equation removeLastEquationFromUseLists(Term representative);

    // Lookup
    Equation getLookup(Term a, Term b);
    void setLookup(Term a, Term b, Equation equation);

    // OtherLookup
    Term otherGetLookup(Term a, Term b);
    void otherSetLookup(Term a, Term b, Term c);

    //
    void propagate();
    void merge(Equation equation);

public:
    void initialize(FunctionSet funcSet, VariableSet varSet, TermSet flattenerSet);
    void initialize(vector<string> equationStrings, FunctionSet* funcSet,
                    VariableSet* varSet, TermSet* flattenerSet, TermMap *flattenMap);
    ClassList getAllClassLists();

    // used for algorithm in paper 2003 - CongruenceClosure with Integer Offsets
    void otherInitialize(FunctionSet funcSet, VariableSet varSet, TermSet flattenerSet, EquationSet eqSet);
    void otherPropagate();
    Term otherNormalize(Term term);

    //
    vector<vector<Term> > findCC(vector<string> equationStrings);
    Term normalize(Term term);

    // explain
    Node* makeNode(Term a);
    Node* findNode(Term a);
    void explain(Term c1, Term c2);
    void explainAlongPath(Term a, Term c);
    void printForest();


    // other
    void printClassLists();
    void printUseLists();
    void printFlattenMap();
    void printRepresentativeMap();
    void printLookupTable();
};

#endif /* FASTCC_H_ */
